$\forall$$A$:Type, $f$:($A$$\rightarrow\mathbb{B}$), $L$:$A$ List, $a$:$A$.
\\[0ex]($a$ $\in$ $L$) $\Rightarrow$ $f$($a$) $\Rightarrow$ ($\forall$$b$:$A$. $a$ before $b$ $\in$ $L$ $\Rightarrow$ $f$($b$)) $\Rightarrow$ ($a$ $\in$ 2of(split\_tail($L$ $\mid$ $\forall$$x$.$f$($x$))))